mcsta/modest mcsta crowds.jani -E TotalRuns=6,CrowdSize=20 --props positive -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --alg OptimisticValueIteration --epsilon 1e-6 --width 1e-6 --relative-width --p0 --p1
crowds.jani:model: info: crowds is a DTMC model.
crowds.jani: info: Need 40 bytes per state.
crowds.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
crowds.jani: info: Explored 10291282 states for TotalRuns=6, CrowdSize=20.
Peak memory usage: 3439 MB
Analysis results for crowds.jani
Experiment TotalRuns=6, CrowdSize=20
+ State space exploration
State size: 40 bytes
States: 10291282
Transitions: 10291282
Branches: 37068802
Rate: 389615 states/s
Time: 27.7 s
+ Property positive
Probability: 0.12047644952814439
Bounds: [0.12047636079718202, 0.12047653825910676]
Time: 10.2 s
+ Precomputations
Min. prob. 0 states: 8587502
Time for min. prob. 0 states: 2.5 s
Min. prob. 1 states: 21252
Time for min. prob. 1 states: 0.4 s
+ Essential states
Iterations: 2
Essential states: 1275122
Transitions: 1275122
Branches: 10200962
Time: 1.3 s
+ Optimistic value iteration
Total iterations: 75
Verif. attempts: 2
Verif. iterations: 8
Final epsilon: 1.188701568812095E-07
Time: 6.0 s
Exported results to file "/out.txt".